T:Type, R:(TT), P:(T).
(x, y:T. (R(x,y))  (P(x) & P(y)))  (x, y:T. (R^+(x,y))  (P(x) & P(y))) 

latex

Definitions	, Type, R^+, x:A. B(x), P  Q, x:AB(x), P & Q, x:A  B(x), f(a), x.A(x), t  T, R1 => R2, Trans(T;x,y.E(x;y)), x f y
Lemmas	rel plus minimal